$\forall$${\it es}$:ES, $i$:Id, $R$:(\{$e$:E$\mid$ loc($e$) = $i$\} $\rightarrow\mathbb{P}$), $e$:E.
\\[0ex]($\forall$$e$:E. (loc($e$) = $i$) $\Rightarrow$ Dec($R$($e$)))
\\[0ex]$\Rightarrow$ (loc($e$) = $i$)
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. (${\it e'}$ $\leq$loc $e$  c$\wedge$ $R$(${\it e'}$)))
\\[0ex]$\Rightarrow$ ($\exists$${\it e'}$:E. (${\it e'}$ $\leq$loc $e$  c$\wedge$ ($R$(${\it e'}$) \& ($\forall$${\it e''}$:E. (${\it e'}$ $<$loc ${\it e''}$) $\Rightarrow$ ${\it e''}$ $\leq$loc $e$  $\Rightarrow$ ($\neg$$R$(${\it e''}$))))))